//  Copyright 2011 Charlie Garrett
//
//  Licensed under the Apache License, Version 2.0 (the "License");
//  you may not use this file except in compliance with the License.
//  You may obtain a copy of the License at
//
//  http://www.apache.org/licenses/LICENSE-2.0
//
//  Unless required by applicable law or agreed to in writing, software
//  distributed under the License is distributed on an "AS IS" BASIS,
//  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
//  See the License for the specific language governing permissions and
//  limitations under the License.
//
//  Interpreter.h
//

#ifndef INTERPRETER_H
#define INTERPRETER_H

#include <map>
#include <set>

#include "logic.h"
#include "Instruction.h"
#include "Register.h"
#include "Term.h"
#include "Value.h"

namespace logic {
using namespace std;    

// TODO LIST:
    // Add _list instructions  (CHECK)
    // Add _void instructions  (CHECK)
    // Update other instructions that depend on CONSTANT and LIST cell types   (CHECK)
    // Generate instructions for CONSTANT, LIST types.  (CHECK)
    // Add lists (CHECK), void variables to parser.
    // Optimize away void variables.
    
    
// Shared base class for all interpreters.
class Interpreter {
public:
    // The state of a computation consists of a Heap of data cells, a stack
    // of environments and a set of registers.  The cells can hold variable 
    // references, structure terms or functor descriptors.
    struct Cell {
        enum CellType {
            REF = 0,
            STR = 1,
            FUNCTOR = 2,
            CONSTANT = 3,
            LIST = 4,
        };
        // TODO: We use a separate field for the cell type, but it could be packed into
        // low order bits of the cell value to save space.
        CellType type;
        union {
            // REF and STR cells contain cell references, either the value to
            // which REF is bound, or the location of the functor descriptor
            // for a STR cell.
            // LIST cells point to the heap address of the first element of a list
            // pair, which is followed by the second element.
            Cell *cell;
            // FUNCTOR cells contain functor descriptors and they occur immediately
            // before structure subterms.
            const Functor* functor;
            // CONSTANT cells contain scalar values.
            const Value *constant;
        } value;
        
        Cell() : type(REF) {
            value.cell = NULL;
        }
        
        Cell(const Cell& other) {
            type = other.type;
            switch (type) {
                case REF:
                case STR:
                case LIST:
                    value.cell = other.value.cell;
                    break;
                case FUNCTOR:
                    value.functor = other.value.functor;
                    break;
                case CONSTANT:
                    value.constant = other.value.constant;
                    break;
            }
        }
        
        Cell(CellType type_, Cell *cell) : type(type_) {
            assert(type == REF || type == STR || type == LIST);
            value.cell = cell;
        }
        
        Cell(const Functor *functor) : type(FUNCTOR) {
            value.functor = functor;
        }
        
        Cell(const Value *constant) : type(CONSTANT) {
            value.constant = constant;
        }
        
        void operator=(const Cell &other) {
            type = other.type;
            switch (type) {
                case REF:
                case STR:
                case LIST:
                    value.cell = other.value.cell;
                    break;
                case FUNCTOR:
                    value.functor = other.value.functor;
                    break;
                case CONSTANT:
                    value.constant = other.value.constant;
                    break;
            }
        }
        
        bool IsRef() const;
        bool IsBoundRef() const;
        bool IsUnboundRef() const;
        void UnbindRef();
        
        bool Equals(const Cell &other);
        
        Cell *deref() const;
        
        string ToString() const;
        string DebugMessage(const Cell *upper_bound) const;
    };
    
    // Two kinds of Frames, Environments and ChoicePoints are maintained on the
    // interpreter's stack.
    struct Frame {
        virtual string ToString() = 0;
    };
    
    // An environment frame contains pointers and permanent variables for active goals.
    struct Environment : public Frame {
        size_t CE;
        vector<Instruction*>::iterator CP;
        size_t num_permanent_vars;
        vector<Cell> Y;
        
        Environment(size_t CE_, vector<Instruction*>::iterator CP_, size_t num_vars);
        
        string ToString();
    };
    
    // A choice point records the WAM state to be restored upon backtracking.
    // Note that choice points outlive the environments in which they are created.
    // In fact, choice points survive when we return with an answer substitution
    // (if there are clauses remaining untried) because the response taken when the
    // user hits ';' is to go back and turn the last successful goal into a failure
    // and resume any untried choices.
    struct ChoicePoint : public Frame {
        vector<Cell> A;     // State of argument registers.
        size_t E;           // Top environment frame.
        size_t B;           // Link in choice point list.
        size_t TR;          // Trail pointer to which we unwind.
        size_t H;           // Top of heap.
        vector<Instruction*>::iterator BP;    // Next clause to try in rule.
        vector<Instruction*>::iterator CP;    // Continuation pointer.
        
        ChoicePoint(size_t E_, size_t B_, size_t TR_, size_t H_, vector<Instruction*>::iterator BP_,
                    vector<Instruction*>::iterator CP_);
        
        string ToString();
    };

    // The heap is a stack of Cells.
    struct State {
        // H is the number of cells pushed onto the heap (i.e. the size).
        size_t H;
        enum { MAX_HEAP_SIZE = 4 * 1024 * 1024 };
        Cell HEAP[MAX_HEAP_SIZE];
        
        // X is the set of temporary registers, which are clobbered by a call.
        vector<Cell> X;
        // A is the set of argument registers, used to pass values to/from a
        // predicate.
        vector<Cell> A;
        
        // Return the next Cell in the heap, or NULL if we reach the limit.
        // The returned Cell should be initialized by the caller.
        Cell *GetNextCell() {
            if (H < MAX_HEAP_SIZE) {
                return &HEAP[H++];
            } else {
                return NULL;
            }
        }
        
        // STACK is the environment stack and E is the index of the top
        // environment on the stack.
        enum { BOTTOM_OF_STACK = 0 };
        vector<Frame*> STACK;
        
        size_t E;
        
        // B is the index of the top choice point on the stack.
        size_t B;
        
        Environment *TopEnvironmentFrame() {
            return static_cast<Environment*>(STACK.at(E));
        }
        
        ChoicePoint *TopChoicePoint() {
            return static_cast<ChoicePoint*>(STACK.at(B));
        }
        
        // TRAIL is a stack of REF Cells that are conditionally bound that will
        // need to be unbound if a choice point is revisited.
        // Note that the TRAIL contains C++ pointers to the Cells to be unbound,
        // unlike the registers sets, which are Cell values that may be REF Cells
        // that contain pointers to other Cells.
        vector<Cell*> TRAIL;
        
        // TR is the index of the top cell on the TRAIL.
        size_t TR;
        
        // HB is the top of the heap (value of H) when we encountered the most
        // recent choice point.  Variables below (or at) HB are trailed but ones
        // above it are not.
        size_t HB;
        
        // When attempting to unify a structure with a structure, we operate
        // in read mode and S is the HEAP location to match against.  When attempting
        // to unify a structure with a variable, we operate in write mode.
        enum UnifyMode {
            UNIFY_READ = 0,
            UNIFY_WRITE = 1
        };
        UnifyMode mode;
        Cell *S;
        
        // When unification fails, this field is set.
        bool fail;
        
        // Number of arguments in current procedure call.
        size_t num_args;
        
        // Instructions in the virtual machine's CODE area.
        vector<Instruction*> code;
        // Next instruction to execute.
        vector<Instruction*>::iterator P;
        // Continuation pointer, where control resumes after a call.
        vector<Instruction*>::iterator CP;

        // The solution to a successful query is the answer substitution mapping
        // variables to values.
        map<Variable*, Cell> answer_substitution;
        
        Cell *CopyCell(const Cell &cell);
        
        void Print() const;
        void PrintAnswer() const;
    };

    State state;
    bool trace;
    
    Interpreter(bool tr = false) : trace(tr) {}

    Cell &GetReg(Register reg);    
    void SetReg(Register reg, const Cell &cell);    
    void CopyReg(Register from, Register to);
    
    // Create cells on the heap and return pointers to them, or NULL if there
    // is no more room on the heap.
    Cell *CreateRefCell();
    Cell *CreateRefCell(Cell *cell);
    Cell *CreateStrCell();
    Cell *CreateFunctorCell(const Functor *functor);
    Cell *CreateListCell(Cell *element);
    Cell *CreateConstantCell(Value *constant);
    Cell *CopyCell(const Cell &cell);
    
    Environment *CreateEnvironment(size_t num_vars);
    
    ChoicePoint *CreateChoicePoint(size_t next_clause_offset);
    void RetryFromChoicePoint(ChoicePoint *choice_point, size_t next_clause_offset);
    
    void EmitInstruction(Instruction *inst) {
        state.code.push_back(inst);
    }
    
    virtual void InitState(bool clear_code = true);
    
    void PrintCode();
    void PrintState();
    void PrintAnswer();
    
    bool Run();
    bool RunFrom(size_t code_offset);
    bool Continue();
    
    // Return true if the interpreter has executed a query and may possibly have
    // another answer through backtracking and false otherwise.
    bool MoreAnswers();
    // Backtrack and try to find more solutions to a query.
    bool FailAndContinue();
    
    // WAM utility routines
    void backtrack();
    void bind(Cell *addr, Cell *ref);
    void trail(Cell *cell);
    void unwind_trail(size_t old_TR, size_t cur_TR);
    void unify(Cell *addr1, Cell *addr2);

    // Machine instructions
    bool put_variable(Register reg, Register arg_reg);
    bool put_value(Register reg, Register arg_reg);
    bool put_structure(const Functor *functor, Register arg_reg);
    bool put_list(Register arg_reg);
    bool put_constant(const Value *constant, Register arg_reg);
    bool get_variable(Register reg, Register arg_reg);
    bool get_value(Register reg, Register arg_reg);
    bool get_list(Register arg_reg);
    bool get_constant(const Value *constant, Register arg_reg);
    bool get_structure(const Functor *functor, Register reg);
    bool set_variable(Register reg);
    bool set_value(Register reg);
    bool set_constant(const Value *constant);
    bool set_void(size_t N);
    bool unify_variable(Register reg);
    bool unify_value(Register reg);
    bool unify_constant(const Value *constant);
    bool unify_void(size_t N);
    bool call(size_t code_offset, size_t nargs);
    bool proceed();
    bool halt();
    bool allocate(size_t N);
    bool deallocate();
    bool try_me_else(size_t next_clause_offset);
    bool retry_me_else(size_t next_clause_offset);
    bool trust_me();
    bool link_source_variable(Variable *var, Register reg);
};

}  // namespace logic

#endif  // L0INTERPRETER_H


